\begin{tabbing}
for\= clients $C$ sends FIFO\+
\\[0ex]from j to i via ($S$[j,i],${\it codes}$)
\\[0ex]receives at i via ($R$[i],${\it decodes}$)  requests ${\it Req}$[j] are acknowledged by ${\it Ack}$[j,i]
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\forall$$i$:$C$.\+
\\[0ex]$\exists$\=$f$:\{$e$:E$\mid$ $R$($i$,$e$)\} $\rightarrow$\{$e$:E$\mid$ $\exists$$j$:$C$. ($S$($j$,$i$,$e$))\} \+
\\[0ex]($\lambda$$e$.$\exists$$j$:$C$. ($S$($j$,$i$,$e$)) $\leftarrow\leftarrow$ $f$$--$ $\lambda$$e$.$R$($i$,$e$)
\\[0ex]\& (\=$\forall$$e$:\{$e$:E$\mid$ $R$($i$,$e$)\} , $j$:\{$j$:$C$$\mid$ $S$($j$,$i$,$f$($e$))\} .\+
\\[0ex]${\it decodes}$($i$,$e$,(state when $e$)) = ${\it codes}$($j$,$i$,$f$($e$),(state when $f$($e$))))
\-\\[0ex]\& (\=$\forall$$e$, ${\it e'}$:\{$e$:E$\mid$ $R$($i$,$e$)\} , $j$:$C$.\+
\\[0ex]($S$($j$,$i$,$f$($e$))) $\Rightarrow$ ($S$($j$,$i$,$f$(${\it e'}$))) $\Rightarrow$ $f$($e$) c$\leq$ $f$(${\it e'}$) $\Rightarrow$ $e$ c$\leq$ ${\it e'}$)
\-\\[0ex]\& (\=$\forall$$j$:$C$.\+
\\[0ex]$\exists$\=${\it req}$:\{$e$:E$\mid$ ${\it Ack}$($j$,$i$,$e$)\} $\rightarrow$\{$e$:E$\mid$ $S$($j$,$i$,$e$) \& ${\it Req}$($j$,$e$)\} \+
\\[0ex]($\lambda$$e$.$S$($j$,$i$,$e$) \& ${\it Req}$($j$,$e$) $\leftarrow\leftarrow$ ${\it req}$$--$ $\lambda$$e$.${\it Ack}$($j$,$i$,$e$)
\\[0ex]\& ($\forall$$a$:\{$e$:E$\mid$ ${\it Ack}$($j$,$i$,$e$)\} . $\exists$$e$:\{$e$:E$\mid$ $R$($i$,$e$)\} . ($f$($e$) = ${\it req}$($a$) \& $e$ c$\leq$ $a$))
\\[0ex]\& $e$.${\it req}$($e$) is c$<$ preserving on $e$.${\it Ack}$($j$,$i$,$e$))))
\-\-\-\-
\end{tabbing}